1.
--subsolver option
/snap/minizinc/current/bin/findMUS -a --output-json --subsolver cp-sat --filter-named LGCols latin_squares.mzn
SubSolver: hard cons: 54 soft cons: 0 leaves: 1 branches: 0 Built tree in 0.05438 seconds.
Background is not satisfiable, exiting. Try using --soft-defines.
2.
--solver option
/snap/minizinc/current/bin/findMUS -a --output-json --solver cp-sat --filter-named LGCols latin_squares.mzn
SubSolver: hard cons: 54 soft cons: 0 leaves: 1 branches: 0 Built tree in 0.05488 seconds.
Background is not satisfiable, exiting. Try using --soft-defines.
3.
Using default solver
/snap/minizinc/current/bin/findMUS -a --output-json --filter-named LGCols latin_squares.mzn
SubSolver: hard cons: 8 soft cons: 2 leaves: 2 branches: 1 Built tree in 0.05401 seconds.
%%%mzn-progress 0.00
%%%mzn-json-start
{"constraints": [
{
"leaf_name": "8",
"name": "gecode_array_int_lt;",
"path": "/mnt/Data/Documents/lab/mus/latin_squares.mzn|22|5|24|9|ca|forall;/mnt/Data/Documents/lab/mus/latin_squares.mzn|22|5|24|9|ac;/mnt/Data/Documents/lab/mus/latin_squares.mzn|22|13|22|13|j=1;/mnt/Data/Documents/lab/mus/latin_squares.mzn|23|10|23|40|ca|\\79@lex_greater",
"assigns": "j=1",
"constraint_name": "LGCols",
"expression_name": "LG(cols 1 2)"
}]
}